Nuprl Lemma : finite-set-type 11,40
T:Type, P:(T).
(x:T. SqStable(P(x)))
 (finite-type({x:T| P(x)} )  (L:T List. (x:T. P(x)  (x  L)))) 
latex

Definitionsx:A. B(x), , P  Q, x(s), P  Q, x:A. B(x), P  Q, t  T, P & Q, S  T, (x  l), A c B, A  B, A, False, T, True, P  Q, {T}, , SqStable(P)
Lemmasiff functionality wrt iff, finite-type wf, l member wf, iff wf, finite-type-iff-list, sq stable wf, select wf, length wf1, cons member

origin